The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#equal(@x, @y) → #eq(@x, @y)
#greater(@x, @y) → #ckgt(#compare(@x, @y))
#less(@x, @y) → #cklt(#compare(@x, @y))
*(@x, @y) → #mult(@x, @y)
+(@x, @y) → #add(@x, @y)
-(@x, @y) → #sub(@x, @y)
add(@b1, @b2) → add'(@b1, @b2, #abs(#0))
add'(@b1, @b2, @r) → add'#1(@b1, @b2, @r)
add'#1(::(@x, @xs), @b2, @r) → add'#2(@b2, @r, @x, @xs)
add'#1(nil, @b2, @r) → nil
add'#2(::(@y, @ys), @r, @x, @xs) → add'#3(sum(@x, @y, @r), @xs, @ys)
add'#2(nil, @r, @x, @xs) → nil
add'#3(tuple#2(@z, @r'), @xs, @ys) → ::(@z, add'(@xs, @ys, @r'))
bitToInt(@b) → bitToInt'(@b, #abs(#pos(#s(#0))))
bitToInt'(@b, @n) → bitToInt'#1(@b, @n)
bitToInt'#1(::(@x, @xs), @n) → +(*(@x, @n), bitToInt'(@xs, *(@n, #pos(#s(#s(#0))))))
bitToInt'#1(nil, @n) → #abs(#0)
compare(@b1, @b2) → compare#1(@b1, @b2)
compare#1(::(@x, @xs), @b2) → compare#2(@b2, @x, @xs)
compare#1(nil, @b2) → #abs(#0)
compare#2(::(@y, @ys), @x, @xs) → compare#3(compare(@xs, @ys), @x, @y)
compare#2(nil, @x, @xs) → #abs(#0)
compare#3(@r, @x, @y) → compare#4(#equal(@r, #0), @r, @x, @y)
compare#4(#false, @r, @x, @y) → @r
compare#4(#true, @r, @x, @y) → compare#5(#less(@x, @y), @x, @y)
compare#5(#false, @x, @y) → compare#6(#greater(@x, @y))
compare#5(#true, @x, @y) → -(#0, #pos(#s(#0)))
compare#6(#false) → #abs(#0)
compare#6(#true) → #abs(#pos(#s(#0)))
diff(@x, @y, @r) → tuple#2(mod(+(+(@x, @y), @r), #pos(#s(#s(#0)))), diff#1(#less(-(-(@x, @y), @r), #0)))
diff#1(#false) → #abs(#0)
diff#1(#true) → #abs(#pos(#s(#0)))
div(@x, @y) → #div(@x, @y)
leq(@b1, @b2) → #less(compare(@b1, @b2), #pos(#s(#0)))
mod(@x, @y) → -(@x, *(@x, div(@x, @y)))
mult(@b1, @b2) → mult#1(@b1, @b2)
mult#1(::(@x, @xs), @b2) → mult#2(::(#abs(#0), mult(@xs, @b2)), @b2, @x)
mult#1(nil, @b2) → nil
mult#2(@zs, @b2, @x) → mult#3(#equal(@x, #pos(#s(#0))), @b2, @zs)
mult#3(#false, @b2, @zs) → @zs
mult#3(#true, @b2, @zs) → add(@b2, @zs)
mult3(@b1, @b2, @b3) → mult(mult(@b1, @b2), @b2)
sub(@b1, @b2) → sub#1(sub'(@b1, @b2, #abs(#0)))
sub#1(tuple#2(@b, @_@1)) → @b
sub'(@b1, @b2, @r) → sub'#1(@b1, @b2, @r)
sub'#1(::(@x, @xs), @b2, @r) → sub'#2(@b2, @r, @x, @xs)
sub'#1(nil, @b2, @r) → tuple#2(nil, @r)
sub'#2(::(@y, @ys), @r, @x, @xs) → sub'#3(diff(@x, @y, @r), @xs, @ys)
sub'#2(nil, @r, @x, @xs) → tuple#2(nil, @r)
sub'#3(tuple#2(@z, @r'), @xs, @ys) → sub'#4(sub'(@xs, @ys, @r'), @z)
sub'#4(tuple#2(@zs, @s), @z) → tuple#2(sub'#5(#equal(@s, #pos(#s(#0))), @z, @zs), @s)
sub'#5(#false, @z, @zs) → ::(@z, @zs)
sub'#5(#true, @z, @zs) → ::(#abs(#0), @zs)
sum(@x, @y, @r) → sum#1(+(+(@x, @y), @r))
sum#1(@s) → sum#2(#equal(@s, #0), @s)
sum#2(#false, @s) → sum#3(#equal(@s, #pos(#s(#0))), @s)
sum#2(#true, @s) → tuple#2(#abs(#0), #abs(#0))
sum#3(#false, @s) → sum#4(#equal(@s, #pos(#s(#s(#0)))))
sum#3(#true, @s) → tuple#2(#abs(#pos(#s(#0))), #abs(#0))
sum#4(#false) → tuple#2(#abs(#pos(#s(#0))), #abs(#pos(#s(#0))))
sum#4(#true) → tuple#2(#abs(#0), #abs(#pos(#s(#0))))

The (relative) TRS S consists of the following rules:

#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#div(#0, #0) → #divByZero
#div(#0, #neg(@y)) → #0
#div(#0, #pos(@y)) → #0
#div(#neg(@x), #0) → #divByZero
#div(#neg(@x), #neg(@y)) → #pos(#natdiv(@x, @y))
#div(#neg(@x), #pos(@y)) → #neg(#natdiv(@x, @y))
#div(#pos(@x), #0) → #divByZero
#div(#pos(@x), #neg(@y)) → #neg(#natdiv(@x, @y))
#div(#pos(@x), #pos(@y)) → #pos(#natdiv(@x, @y))
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#eq(nil, tuple#2(@y_1, @y_2)) → #false
#eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) → #false
#eq(tuple#2(@x_1, @x_2), nil) → #false
#eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natdiv(#0, #0) → #divByZero
#natdiv(#s(@x), #s(@y)) → #s(#natdiv(#natsub(@x, @y), #s(@y)))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#natsub(@x, #0) → @x
#natsub(#s(@x), #s(@y)) → #natsub(@x, @y)
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#sub(@x, #0) → @x
#sub(@x, #neg(@y)) → #add(@x, #pos(@y))
#sub(@x, #pos(@y)) → #add(@x, #neg(@y))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
bitToInt'(::(@x2875451_7, @xs2875452_7), @n) →⁺ +(*(@x2875451_7, @n), bitToInt'(@xs2875452_7, *(@n, #pos(#s(#s(#0))))))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [@xs2875452_7 / ::(@x2875451_7, @xs2875452_7)].
The result substitution is [@n / *(@n, #pos(#s(#s(#0))))].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#equal(@x, @y) → #eq(@x, @y)
#greater(@x, @y) → #ckgt(#compare(@x, @y))
#less(@x, @y) → #cklt(#compare(@x, @y))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
-(@x, @y) → #sub(@x, @y)
add(@b1, @b2) → add'(@b1, @b2, #abs(#0))
add'(@b1, @b2, @r) → add'#1(@b1, @b2, @r)
add'#1(::(@x, @xs), @b2, @r) → add'#2(@b2, @r, @x, @xs)
add'#1(nil, @b2, @r) → nil
add'#2(::(@y, @ys), @r, @x, @xs) → add'#3(sum(@x, @y, @r), @xs, @ys)
add'#2(nil, @r, @x, @xs) → nil
add'#3(tuple#2(@z, @r'), @xs, @ys) → ::(@z, add'(@xs, @ys, @r'))
bitToInt(@b) → bitToInt'(@b, #abs(#pos(#s(#0))))
bitToInt'(@b, @n) → bitToInt'#1(@b, @n)
bitToInt'#1(::(@x, @xs), @n) → +'(*'(@x, @n), bitToInt'(@xs, *'(@n, #pos(#s(#s(#0))))))
bitToInt'#1(nil, @n) → #abs(#0)
compare(@b1, @b2) → compare#1(@b1, @b2)
compare#1(::(@x, @xs), @b2) → compare#2(@b2, @x, @xs)
compare#1(nil, @b2) → #abs(#0)
compare#2(::(@y, @ys), @x, @xs) → compare#3(compare(@xs, @ys), @x, @y)
compare#2(nil, @x, @xs) → #abs(#0)
compare#3(@r, @x, @y) → compare#4(#equal(@r, #0), @r, @x, @y)
compare#4(#false, @r, @x, @y) → @r
compare#4(#true, @r, @x, @y) → compare#5(#less(@x, @y), @x, @y)
compare#5(#false, @x, @y) → compare#6(#greater(@x, @y))
compare#5(#true, @x, @y) → -(#0, #pos(#s(#0)))
compare#6(#false) → #abs(#0)
compare#6(#true) → #abs(#pos(#s(#0)))
diff(@x, @y, @r) → tuple#2(mod(+'(+'(@x, @y), @r), #pos(#s(#s(#0)))), diff#1(#less(-(-(@x, @y), @r), #0)))
diff#1(#false) → #abs(#0)
diff#1(#true) → #abs(#pos(#s(#0)))
div(@x, @y) → #div(@x, @y)
leq(@b1, @b2) → #less(compare(@b1, @b2), #pos(#s(#0)))
mod(@x, @y) → -(@x, *'(@x, div(@x, @y)))
mult(@b1, @b2) → mult#1(@b1, @b2)
mult#1(::(@x, @xs), @b2) → mult#2(::(#abs(#0), mult(@xs, @b2)), @b2, @x)
mult#1(nil, @b2) → nil
mult#2(@zs, @b2, @x) → mult#3(#equal(@x, #pos(#s(#0))), @b2, @zs)
mult#3(#false, @b2, @zs) → @zs
mult#3(#true, @b2, @zs) → add(@b2, @zs)
mult3(@b1, @b2, @b3) → mult(mult(@b1, @b2), @b2)
sub(@b1, @b2) → sub#1(sub'(@b1, @b2, #abs(#0)))
sub#1(tuple#2(@b, @_@1)) → @b
sub'(@b1, @b2, @r) → sub'#1(@b1, @b2, @r)
sub'#1(::(@x, @xs), @b2, @r) → sub'#2(@b2, @r, @x, @xs)
sub'#1(nil, @b2, @r) → tuple#2(nil, @r)
sub'#2(::(@y, @ys), @r, @x, @xs) → sub'#3(diff(@x, @y, @r), @xs, @ys)
sub'#2(nil, @r, @x, @xs) → tuple#2(nil, @r)
sub'#3(tuple#2(@z, @r'), @xs, @ys) → sub'#4(sub'(@xs, @ys, @r'), @z)
sub'#4(tuple#2(@zs, @s), @z) → tuple#2(sub'#5(#equal(@s, #pos(#s(#0))), @z, @zs), @s)
sub'#5(#false, @z, @zs) → ::(@z, @zs)
sub'#5(#true, @z, @zs) → ::(#abs(#0), @zs)
sum(@x, @y, @r) → sum#1(+'(+'(@x, @y), @r))
sum#1(@s) → sum#2(#equal(@s, #0), @s)
sum#2(#false, @s) → sum#3(#equal(@s, #pos(#s(#0))), @s)
sum#2(#true, @s) → tuple#2(#abs(#0), #abs(#0))
sum#3(#false, @s) → sum#4(#equal(@s, #pos(#s(#s(#0)))))
sum#3(#true, @s) → tuple#2(#abs(#pos(#s(#0))), #abs(#0))
sum#4(#false) → tuple#2(#abs(#pos(#s(#0))), #abs(#pos(#s(#0))))
sum#4(#true) → tuple#2(#abs(#0), #abs(#pos(#s(#0))))

The (relative) TRS S consists of the following rules:

#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#div(#0, #0) → #divByZero
#div(#0, #neg(@y)) → #0
#div(#0, #pos(@y)) → #0
#div(#neg(@x), #0) → #divByZero
#div(#neg(@x), #neg(@y)) → #pos(#natdiv(@x, @y))
#div(#neg(@x), #pos(@y)) → #neg(#natdiv(@x, @y))
#div(#pos(@x), #0) → #divByZero
#div(#pos(@x), #neg(@y)) → #neg(#natdiv(@x, @y))
#div(#pos(@x), #pos(@y)) → #pos(#natdiv(@x, @y))
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#eq(nil, tuple#2(@y_1, @y_2)) → #false
#eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) → #false
#eq(tuple#2(@x_1, @x_2), nil) → #false
#eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natdiv(#0, #0) → #divByZero
#natdiv(#s(@x), #s(@y)) → #s(#natdiv(#natsub(@x, @y), #s(@y)))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#natsub(@x, #0) → @x
#natsub(#s(@x), #s(@y)) → #natsub(@x, @y)
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#sub(@x, #0) → @x
#sub(@x, #neg(@y)) → #add(@x, #pos(@y))
#sub(@x, #pos(@y)) → #add(@x, #neg(@y))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Rewrite Strategy: INNERMOST

(5) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
mult3/2

(6) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#equal(@x, @y) → #eq(@x, @y)
#greater(@x, @y) → #ckgt(#compare(@x, @y))
#less(@x, @y) → #cklt(#compare(@x, @y))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
-(@x, @y) → #sub(@x, @y)
add(@b1, @b2) → add'(@b1, @b2, #abs(#0))
add'(@b1, @b2, @r) → add'#1(@b1, @b2, @r)
add'#1(::(@x, @xs), @b2, @r) → add'#2(@b2, @r, @x, @xs)
add'#1(nil, @b2, @r) → nil
add'#2(::(@y, @ys), @r, @x, @xs) → add'#3(sum(@x, @y, @r), @xs, @ys)
add'#2(nil, @r, @x, @xs) → nil
add'#3(tuple#2(@z, @r'), @xs, @ys) → ::(@z, add'(@xs, @ys, @r'))
bitToInt(@b) → bitToInt'(@b, #abs(#pos(#s(#0))))
bitToInt'(@b, @n) → bitToInt'#1(@b, @n)
bitToInt'#1(::(@x, @xs), @n) → +'(*'(@x, @n), bitToInt'(@xs, *'(@n, #pos(#s(#s(#0))))))
bitToInt'#1(nil, @n) → #abs(#0)
compare(@b1, @b2) → compare#1(@b1, @b2)
compare#1(::(@x, @xs), @b2) → compare#2(@b2, @x, @xs)
compare#1(nil, @b2) → #abs(#0)
compare#2(::(@y, @ys), @x, @xs) → compare#3(compare(@xs, @ys), @x, @y)
compare#2(nil, @x, @xs) → #abs(#0)
compare#3(@r, @x, @y) → compare#4(#equal(@r, #0), @r, @x, @y)
compare#4(#false, @r, @x, @y) → @r
compare#4(#true, @r, @x, @y) → compare#5(#less(@x, @y), @x, @y)
compare#5(#false, @x, @y) → compare#6(#greater(@x, @y))
compare#5(#true, @x, @y) → -(#0, #pos(#s(#0)))
compare#6(#false) → #abs(#0)
compare#6(#true) → #abs(#pos(#s(#0)))
diff(@x, @y, @r) → tuple#2(mod(+'(+'(@x, @y), @r), #pos(#s(#s(#0)))), diff#1(#less(-(-(@x, @y), @r), #0)))
diff#1(#false) → #abs(#0)
diff#1(#true) → #abs(#pos(#s(#0)))
div(@x, @y) → #div(@x, @y)
leq(@b1, @b2) → #less(compare(@b1, @b2), #pos(#s(#0)))
mod(@x, @y) → -(@x, *'(@x, div(@x, @y)))
mult(@b1, @b2) → mult#1(@b1, @b2)
mult#1(::(@x, @xs), @b2) → mult#2(::(#abs(#0), mult(@xs, @b2)), @b2, @x)
mult#1(nil, @b2) → nil
mult#2(@zs, @b2, @x) → mult#3(#equal(@x, #pos(#s(#0))), @b2, @zs)
mult#3(#false, @b2, @zs) → @zs
mult#3(#true, @b2, @zs) → add(@b2, @zs)
mult3(@b1, @b2) → mult(mult(@b1, @b2), @b2)
sub(@b1, @b2) → sub#1(sub'(@b1, @b2, #abs(#0)))
sub#1(tuple#2(@b, @_@1)) → @b
sub'(@b1, @b2, @r) → sub'#1(@b1, @b2, @r)
sub'#1(::(@x, @xs), @b2, @r) → sub'#2(@b2, @r, @x, @xs)
sub'#1(nil, @b2, @r) → tuple#2(nil, @r)
sub'#2(::(@y, @ys), @r, @x, @xs) → sub'#3(diff(@x, @y, @r), @xs, @ys)
sub'#2(nil, @r, @x, @xs) → tuple#2(nil, @r)
sub'#3(tuple#2(@z, @r'), @xs, @ys) → sub'#4(sub'(@xs, @ys, @r'), @z)
sub'#4(tuple#2(@zs, @s), @z) → tuple#2(sub'#5(#equal(@s, #pos(#s(#0))), @z, @zs), @s)
sub'#5(#false, @z, @zs) → ::(@z, @zs)
sub'#5(#true, @z, @zs) → ::(#abs(#0), @zs)
sum(@x, @y, @r) → sum#1(+'(+'(@x, @y), @r))
sum#1(@s) → sum#2(#equal(@s, #0), @s)
sum#2(#false, @s) → sum#3(#equal(@s, #pos(#s(#0))), @s)
sum#2(#true, @s) → tuple#2(#abs(#0), #abs(#0))
sum#3(#false, @s) → sum#4(#equal(@s, #pos(#s(#s(#0)))))
sum#3(#true, @s) → tuple#2(#abs(#pos(#s(#0))), #abs(#0))
sum#4(#false) → tuple#2(#abs(#pos(#s(#0))), #abs(#pos(#s(#0))))
sum#4(#true) → tuple#2(#abs(#0), #abs(#pos(#s(#0))))

The (relative) TRS S consists of the following rules:

#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#div(#0, #0) → #divByZero
#div(#0, #neg(@y)) → #0
#div(#0, #pos(@y)) → #0
#div(#neg(@x), #0) → #divByZero
#div(#neg(@x), #neg(@y)) → #pos(#natdiv(@x, @y))
#div(#neg(@x), #pos(@y)) → #neg(#natdiv(@x, @y))
#div(#pos(@x), #0) → #divByZero
#div(#pos(@x), #neg(@y)) → #neg(#natdiv(@x, @y))
#div(#pos(@x), #pos(@y)) → #pos(#natdiv(@x, @y))
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#eq(nil, tuple#2(@y_1, @y_2)) → #false
#eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) → #false
#eq(tuple#2(@x_1, @x_2), nil) → #false
#eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natdiv(#0, #0) → #divByZero
#natdiv(#s(@x), #s(@y)) → #s(#natdiv(#natsub(@x, @y), #s(@y)))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#natsub(@x, #0) → @x
#natsub(#s(@x), #s(@y)) → #natsub(@x, @y)
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#sub(@x, #0) → @x
#sub(@x, #neg(@y)) → #add(@x, #pos(@y))
#sub(@x, #pos(@y)) → #add(@x, #neg(@y))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Rewrite Strategy: INNERMOST

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(8) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#equal(@x, @y) → #eq(@x, @y)
#greater(@x, @y) → #ckgt(#compare(@x, @y))
#less(@x, @y) → #cklt(#compare(@x, @y))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
-(@x, @y) → #sub(@x, @y)
add(@b1, @b2) → add'(@b1, @b2, #abs(#0))
add'(@b1, @b2, @r) → add'#1(@b1, @b2, @r)
add'#1(::(@x, @xs), @b2, @r) → add'#2(@b2, @r, @x, @xs)
add'#1(nil, @b2, @r) → nil
add'#2(::(@y, @ys), @r, @x, @xs) → add'#3(sum(@x, @y, @r), @xs, @ys)
add'#2(nil, @r, @x, @xs) → nil
add'#3(tuple#2(@z, @r'), @xs, @ys) → ::(@z, add'(@xs, @ys, @r'))
bitToInt(@b) → bitToInt'(@b, #abs(#pos(#s(#0))))
bitToInt'(@b, @n) → bitToInt'#1(@b, @n)
bitToInt'#1(::(@x, @xs), @n) → +'(*'(@x, @n), bitToInt'(@xs, *'(@n, #pos(#s(#s(#0))))))
bitToInt'#1(nil, @n) → #abs(#0)
compare(@b1, @b2) → compare#1(@b1, @b2)
compare#1(::(@x, @xs), @b2) → compare#2(@b2, @x, @xs)
compare#1(nil, @b2) → #abs(#0)
compare#2(::(@y, @ys), @x, @xs) → compare#3(compare(@xs, @ys), @x, @y)
compare#2(nil, @x, @xs) → #abs(#0)
compare#3(@r, @x, @y) → compare#4(#equal(@r, #0), @r, @x, @y)
compare#4(#false, @r, @x, @y) → @r
compare#4(#true, @r, @x, @y) → compare#5(#less(@x, @y), @x, @y)
compare#5(#false, @x, @y) → compare#6(#greater(@x, @y))
compare#5(#true, @x, @y) → -(#0, #pos(#s(#0)))
compare#6(#false) → #abs(#0)
compare#6(#true) → #abs(#pos(#s(#0)))
diff(@x, @y, @r) → tuple#2(mod(+'(+'(@x, @y), @r), #pos(#s(#s(#0)))), diff#1(#less(-(-(@x, @y), @r), #0)))
diff#1(#false) → #abs(#0)
diff#1(#true) → #abs(#pos(#s(#0)))
div(@x, @y) → #div(@x, @y)
leq(@b1, @b2) → #less(compare(@b1, @b2), #pos(#s(#0)))
mod(@x, @y) → -(@x, *'(@x, div(@x, @y)))
mult(@b1, @b2) → mult#1(@b1, @b2)
mult#1(::(@x, @xs), @b2) → mult#2(::(#abs(#0), mult(@xs, @b2)), @b2, @x)
mult#1(nil, @b2) → nil
mult#2(@zs, @b2, @x) → mult#3(#equal(@x, #pos(#s(#0))), @b2, @zs)
mult#3(#false, @b2, @zs) → @zs
mult#3(#true, @b2, @zs) → add(@b2, @zs)
mult3(@b1, @b2) → mult(mult(@b1, @b2), @b2)
sub(@b1, @b2) → sub#1(sub'(@b1, @b2, #abs(#0)))
sub#1(tuple#2(@b, @_@1)) → @b
sub'(@b1, @b2, @r) → sub'#1(@b1, @b2, @r)
sub'#1(::(@x, @xs), @b2, @r) → sub'#2(@b2, @r, @x, @xs)
sub'#1(nil, @b2, @r) → tuple#2(nil, @r)
sub'#2(::(@y, @ys), @r, @x, @xs) → sub'#3(diff(@x, @y, @r), @xs, @ys)
sub'#2(nil, @r, @x, @xs) → tuple#2(nil, @r)
sub'#3(tuple#2(@z, @r'), @xs, @ys) → sub'#4(sub'(@xs, @ys, @r'), @z)
sub'#4(tuple#2(@zs, @s), @z) → tuple#2(sub'#5(#equal(@s, #pos(#s(#0))), @z, @zs), @s)
sub'#5(#false, @z, @zs) → ::(@z, @zs)
sub'#5(#true, @z, @zs) → ::(#abs(#0), @zs)
sum(@x, @y, @r) → sum#1(+'(+'(@x, @y), @r))
sum#1(@s) → sum#2(#equal(@s, #0), @s)
sum#2(#false, @s) → sum#3(#equal(@s, #pos(#s(#0))), @s)
sum#2(#true, @s) → tuple#2(#abs(#0), #abs(#0))
sum#3(#false, @s) → sum#4(#equal(@s, #pos(#s(#s(#0)))))
sum#3(#true, @s) → tuple#2(#abs(#pos(#s(#0))), #abs(#0))
sum#4(#false) → tuple#2(#abs(#pos(#s(#0))), #abs(#pos(#s(#0))))
sum#4(#true) → tuple#2(#abs(#0), #abs(#pos(#s(#0))))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#div(#0, #0) → #divByZero
#div(#0, #neg(@y)) → #0
#div(#0, #pos(@y)) → #0
#div(#neg(@x), #0) → #divByZero
#div(#neg(@x), #neg(@y)) → #pos(#natdiv(@x, @y))
#div(#neg(@x), #pos(@y)) → #neg(#natdiv(@x, @y))
#div(#pos(@x), #0) → #divByZero
#div(#pos(@x), #neg(@y)) → #neg(#natdiv(@x, @y))
#div(#pos(@x), #pos(@y)) → #pos(#natdiv(@x, @y))
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#eq(nil, tuple#2(@y_1, @y_2)) → #false
#eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) → #false
#eq(tuple#2(@x_1, @x_2), nil) → #false
#eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natdiv(#0, #0) → #divByZero
#natdiv(#s(@x), #s(@y)) → #s(#natdiv(#natsub(@x, @y), #s(@y)))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#natsub(@x, #0) → @x
#natsub(#s(@x), #s(@y)) → #natsub(@x, @y)
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#sub(@x, #0) → @x
#sub(@x, #neg(@y)) → #add(@x, #pos(@y))
#sub(@x, #pos(@y)) → #add(@x, #neg(@y))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#0 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#neg :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#pos :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#s :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#equal :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #false:#true
#eq :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #false:#true
#greater :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #EQ:#GT:#LT
#less :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
*' :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#mult :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
+' :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#add :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
- :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#sub :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
add :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
add' :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
add'#1 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
:: :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
add'#2 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
nil :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
add'#3 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sum :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
tuple#2 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
bitToInt :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
bitToInt' :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
bitToInt'#1 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
compare :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
compare#1 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
compare#2 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
compare#3 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
compare#4 :: #false:#true → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#false :: #false:#true
#true :: #false:#true
compare#5 :: #false:#true → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
compare#6 :: #false:#true → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
diff :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
mod :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
diff#1 :: #false:#true → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
div :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#div :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
leq :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #false:#true
mult :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
mult#1 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
mult#2 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
mult#3 :: #false:#true → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
mult3 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sub :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sub#1 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sub' :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sub'#1 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sub'#2 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sub'#3 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sub'#4 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sub'#5 :: #false:#true → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sum#1 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sum#2 :: #false:#true → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sum#3 :: #false:#true → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sum#4 :: #false:#true → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#pred :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#succ :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#and :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#divByZero :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#natdiv :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#natmult :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#natsub :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
hole_#0:#neg:#pos:#s::::nil:tuple#2:#divByZero1_7 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
hole_#false:#true2_7 :: #false:#true
hole_#EQ:#GT:#LT3_7 :: #EQ:#GT:#LT
gen_#0:#neg:#pos:#s::::nil:tuple#2:#divByZero4_7 :: Nat → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero

(9) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
#eq, #compare, #add, add', add'#1, add'#3, bitToInt', bitToInt'#1, compare, compare#1, mult, mult#1, sub', sub'#1, sub'#3, #natdiv, #natmult, #natsub

They will be analysed ascendingly in the following order:
#add < #natmult
add' = add'#1
add' = add'#3
add'#1 = add'#3
bitToInt' = bitToInt'#1
compare = compare#1
mult = mult#1
sub' = sub'#1
sub' = sub'#3
sub'#1 = sub'#3
#natsub < #natdiv

(10) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#equal(@x, @y) → #eq(@x, @y)
#greater(@x, @y) → #ckgt(#compare(@x, @y))
#less(@x, @y) → #cklt(#compare(@x, @y))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
-(@x, @y) → #sub(@x, @y)
add(@b1, @b2) → add'(@b1, @b2, #abs(#0))
add'(@b1, @b2, @r) → add'#1(@b1, @b2, @r)
add'#1(::(@x, @xs), @b2, @r) → add'#2(@b2, @r, @x, @xs)
add'#1(nil, @b2, @r) → nil
add'#2(::(@y, @ys), @r, @x, @xs) → add'#3(sum(@x, @y, @r), @xs, @ys)
add'#2(nil, @r, @x, @xs) → nil
add'#3(tuple#2(@z, @r'), @xs, @ys) → ::(@z, add'(@xs, @ys, @r'))
bitToInt(@b) → bitToInt'(@b, #abs(#pos(#s(#0))))
bitToInt'(@b, @n) → bitToInt'#1(@b, @n)
bitToInt'#1(::(@x, @xs), @n) → +'(*'(@x, @n), bitToInt'(@xs, *'(@n, #pos(#s(#s(#0))))))
bitToInt'#1(nil, @n) → #abs(#0)
compare(@b1, @b2) → compare#1(@b1, @b2)
compare#1(::(@x, @xs), @b2) → compare#2(@b2, @x, @xs)
compare#1(nil, @b2) → #abs(#0)
compare#2(::(@y, @ys), @x, @xs) → compare#3(compare(@xs, @ys), @x, @y)
compare#2(nil, @x, @xs) → #abs(#0)
compare#3(@r, @x, @y) → compare#4(#equal(@r, #0), @r, @x, @y)
compare#4(#false, @r, @x, @y) → @r
compare#4(#true, @r, @x, @y) → compare#5(#less(@x, @y), @x, @y)
compare#5(#false, @x, @y) → compare#6(#greater(@x, @y))
compare#5(#true, @x, @y) → -(#0, #pos(#s(#0)))
compare#6(#false) → #abs(#0)
compare#6(#true) → #abs(#pos(#s(#0)))
diff(@x, @y, @r) → tuple#2(mod(+'(+'(@x, @y), @r), #pos(#s(#s(#0)))), diff#1(#less(-(-(@x, @y), @r), #0)))
diff#1(#false) → #abs(#0)
diff#1(#true) → #abs(#pos(#s(#0)))
div(@x, @y) → #div(@x, @y)
leq(@b1, @b2) → #less(compare(@b1, @b2), #pos(#s(#0)))
mod(@x, @y) → -(@x, *'(@x, div(@x, @y)))
mult(@b1, @b2) → mult#1(@b1, @b2)
mult#1(::(@x, @xs), @b2) → mult#2(::(#abs(#0), mult(@xs, @b2)), @b2, @x)
mult#1(nil, @b2) → nil
mult#2(@zs, @b2, @x) → mult#3(#equal(@x, #pos(#s(#0))), @b2, @zs)
mult#3(#false, @b2, @zs) → @zs
mult#3(#true, @b2, @zs) → add(@b2, @zs)
mult3(@b1, @b2) → mult(mult(@b1, @b2), @b2)
sub(@b1, @b2) → sub#1(sub'(@b1, @b2, #abs(#0)))
sub#1(tuple#2(@b, @_@1)) → @b
sub'(@b1, @b2, @r) → sub'#1(@b1, @b2, @r)
sub'#1(::(@x, @xs), @b2, @r) → sub'#2(@b2, @r, @x, @xs)
sub'#1(nil, @b2, @r) → tuple#2(nil, @r)
sub'#2(::(@y, @ys), @r, @x, @xs) → sub'#3(diff(@x, @y, @r), @xs, @ys)
sub'#2(nil, @r, @x, @xs) → tuple#2(nil, @r)
sub'#3(tuple#2(@z, @r'), @xs, @ys) → sub'#4(sub'(@xs, @ys, @r'), @z)
sub'#4(tuple#2(@zs, @s), @z) → tuple#2(sub'#5(#equal(@s, #pos(#s(#0))), @z, @zs), @s)
sub'#5(#false, @z, @zs) → ::(@z, @zs)
sub'#5(#true, @z, @zs) → ::(#abs(#0), @zs)
sum(@x, @y, @r) → sum#1(+'(+'(@x, @y), @r))
sum#1(@s) → sum#2(#equal(@s, #0), @s)
sum#2(#false, @s) → sum#3(#equal(@s, #pos(#s(#0))), @s)
sum#2(#true, @s) → tuple#2(#abs(#0), #abs(#0))
sum#3(#false, @s) → sum#4(#equal(@s, #pos(#s(#s(#0)))))
sum#3(#true, @s) → tuple#2(#abs(#pos(#s(#0))), #abs(#0))
sum#4(#false) → tuple#2(#abs(#pos(#s(#0))), #abs(#pos(#s(#0))))
sum#4(#true) → tuple#2(#abs(#0), #abs(#pos(#s(#0))))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#div(#0, #0) → #divByZero
#div(#0, #neg(@y)) → #0
#div(#0, #pos(@y)) → #0
#div(#neg(@x), #0) → #divByZero
#div(#neg(@x), #neg(@y)) → #pos(#natdiv(@x, @y))
#div(#neg(@x), #pos(@y)) → #neg(#natdiv(@x, @y))
#div(#pos(@x), #0) → #divByZero
#div(#pos(@x), #neg(@y)) → #neg(#natdiv(@x, @y))
#div(#pos(@x), #pos(@y)) → #pos(#natdiv(@x, @y))
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#eq(nil, tuple#2(@y_1, @y_2)) → #false
#eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) → #false
#eq(tuple#2(@x_1, @x_2), nil) → #false
#eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natdiv(#0, #0) → #divByZero
#natdiv(#s(@x), #s(@y)) → #s(#natdiv(#natsub(@x, @y), #s(@y)))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#natsub(@x, #0) → @x
#natsub(#s(@x), #s(@y)) → #natsub(@x, @y)
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#sub(@x, #0) → @x
#sub(@x, #neg(@y)) → #add(@x, #pos(@y))
#sub(@x, #pos(@y)) → #add(@x, #neg(@y))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#0 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#neg :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#pos :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#s :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#equal :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #false:#true
#eq :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #false:#true
#greater :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #EQ:#GT:#LT
#less :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
*' :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#mult :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
+' :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#add :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
- :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#sub :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
add :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
add' :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
add'#1 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
:: :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
add'#2 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
nil :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
add'#3 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sum :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
tuple#2 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
bitToInt :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
bitToInt' :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
bitToInt'#1 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
compare :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
compare#1 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
compare#2 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
compare#3 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
compare#4 :: #false:#true → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#false :: #false:#true
#true :: #false:#true
compare#5 :: #false:#true → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
compare#6 :: #false:#true → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
diff :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
mod :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
diff#1 :: #false:#true → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
div :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#div :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
leq :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #false:#true
mult :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
mult#1 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
mult#2 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
mult#3 :: #false:#true → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
mult3 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sub :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sub#1 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sub' :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sub'#1 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sub'#2 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sub'#3 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sub'#4 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sub'#5 :: #false:#true → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sum#1 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sum#2 :: #false:#true → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sum#3 :: #false:#true → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
sum#4 :: #false:#true → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#pred :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#succ :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#and :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#divByZero :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#natdiv :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#natmult :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
#natsub :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
hole_#0:#neg:#pos:#s::::nil:tuple#2:#divByZero1_7 :: #0:#neg:#pos:#s::::nil:tuple#2:#divByZero
hole_#false:#true2_7 :: #false:#true
hole_#EQ:#GT:#LT3_7 :: #EQ:#GT:#LT
gen_#0:#neg:#pos:#s::::nil:tuple#2:#divByZero4_7 :: Nat → #0:#neg:#pos:#s::::nil:tuple#2:#divByZero

Generator Equations:
gen_#0:#neg:#pos:#s::::nil:tuple#2:#divByZero4_7(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil:tuple#2:#divByZero4_7(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil:tuple#2:#divByZero4_7(x))

The following defined symbols remain to be analysed:
#eq, #compare, #add, add', add'#1, add'#3, bitToInt', bitToInt'#1, compare, compare#1, mult, mult#1, sub', sub'#1, sub'#3, #natdiv, #natmult, #natsub

They will be analysed ascendingly in the following order:
#add < #natmult
add' = add'#1
add' = add'#3
add'#1 = add'#3
bitToInt' = bitToInt'#1
compare = compare#1
mult = mult#1
sub' = sub'#1
sub' = sub'#3
sub'#1 = sub'#3
#natsub < #natdiv